$\forall$$r$:(Id$\rightarrow$Id), $f$:$a$:Id fp$\rightarrow$ Type, $a$:Id, $z$:Type.
\\[0ex]Inj(Id; Id; $r$) $\Rightarrow$ rename($r$;$f$)($r$($a$))?$z$ $=$ $f$($a$)?$z$ $\in$ Type